(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2.
The certificate found is represented by the following graph.
Start state: 1277
Accept states: [1278, 1279, 1280]
Transitions:
1277→1278[a_1|0]
1277→1279[b_1|0]
1277→1280[Q_1|0]
1277→1277[P_1|0, x_1|0]
1277→1281[x_1|1]
1277→1283[Q_1|1]
1277→1284[a_1|1]
1277→1285[Q_1|1]
1277→1286[a_1|2]
1281→1282[a_1|1]
1282→1278[P_1|1]
1282→1284[P_1|1]
1282→1286[P_1|1]
1283→1279[b_1|1]
1284→1278[x_1|1]
1284→1284[x_1|1]
1284→1286[x_1|1]
1285→1280[a_1|1]
1285→1283[a_1|1]
1285→1285[a_1|1]
1286→1282[x_1|2]